1. Technical Field
The present invention relates to model checking for software and hardware and more particularly to a system and method for more efficiently validating models using application-aware satisfiability checkers.
2. Description of the Related Art
In application domains such as model checking of software and hardware, an analysis engine has to explore paths of bounded length to validate a reachability property. The core of the analysis engine typically uses a Davis Putnam Longman Loveland (DPLL) based satisfiability (SAT) solver to search through the path formula. As the paths get longer, the number of possible paths increases exponentially. This leads to an increase in formula size, and the search space; thereby, affecting the performance of the analysis engine.
Current SAT solvers use various techniques such as frequent restarts, branching heuristics, and conflict-driven learning to prune the search space faster. Other techniques include learning clauses such as conflict-driven resolution clauses and binary clauses. These solvers also rely on other features such as two-literal watch scheme, table lookup, efficient preprocessing, hybrid representation, and many others. However, these techniques are based on heuristics that are derived from a given formula. These techniques may become inefficient due to excessive restarts and branching. Such approaches do not consider application specific information to guide the search.